$\forall$$w$:World. \\[0ex]FairFifo \\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\lambda$$x$.state\_when($e$)($x$,0)) = ($\lambda$$x$.s(loc($e$);time($e$)).$x$(0)) $\in$ $x$:Id$\rightarrow$vartype(loc($e$);$x$))